% exception for AKA
consneeded(pri(aka,[KA,N1,KB,N2]),[KAP,N1,KB,N2]) :- KAP=pri(pk,[KA]).
consneeded(pri(aka,[KA,N1,KB,N2]),[KA,N1,KBP,N2]) :- KBP=pri(pk,[KB]), !.

% normal construction rule
consneeded(pri(_,L),L).

% list
elneeded(pri(lst,L),X,[]) :- member(X,L).

% symmetric encryption
elneeded(pri(enc,[M,K]),M,[K]).

% asymmetric encryption
elneeded(pri(aenc,[M,pri(pk,[KI])]),M,[KI]).

% labelled asymmetric encryption
elneeded(pri(aencl,[M,pri(pk,[KI]),_]),M,[KI]).
elneeded(pri(aencl,[_,_,L]),L,[]).

% signature
elneeded(pri(sig,[M,KM]),M,[pri(pk,[KM])]).
elneeded(pri(sig,[_,KM]),pri(pk,[KM]),[pri(pk,[KM])]).

% zero-knowledge proof
elneeded(pri(zk,[_,M2,_,_]),M2,[]).
elneeded(pri(zk,[M1,_,NP,_]),M1,[NP]).

% anonymous credential
elneeded(pri(cred,[I,KM,D,_,_]),pri(pk,[KM]),[pri(pk,[KM]),I,D]).

% anonymous credential issuing protocol
elneeded(pri(icred,[I,KM,D,_ ,NO,_ ,_ ,NI,_ ,_ ]),pri(cred,[I,KM,D,NO,NI]),[NO]).
elneeded(pri(icred,[I,_ ,_,_ ,_ ,N3,_ ,_ ,_ ,_ ]),I,[N3]).
elneeded(pri(icred,[_,_ ,_,N1,_ ,N3,_ ,_ ,_ ,_ ]),N1,[N3]).
elneeded(pri(icred,[_,_ ,_,_ ,NO,N3,_ ,_ ,_ ,_ ]),NO,[N3]).
elneeded(pri(icred,[_,KM,_,_ ,_ ,_ ,_ ,_ ,N6,_ ]),KM,[N6]).
elneeded(pri(icred,[_,KM,_,_ ,_ ,_ ,_ ,_ ,_ ,_ ]),pri(pk,[KM]),  []).
elneeded(pri(icred,[I,_ ,_,N1,_ ,_ ,_ ,_ ,_ ,_ ]),pri(rc,[I,N1]),[]).
elneeded(pri(icred,[_,_ ,D,_ ,_ ,_ ,_ ,_ ,_ ,_ ]),D,             []).
elneeded(pri(icred,[I,_ ,_,_ ,NO,_ ,_ ,_ ,_ ,_ ]),I,             [I,NO]).
elneeded(pri(icred,[I,_ ,_,_ ,NO,_ ,_ ,_ ,_ ,_ ]),NO,            [I,NO]).
elneeded(pri(icred,[I,KM,D,_ ,NO,_ ,_ ,NI,_ ,_ ]),pri(cred,[I,KM,D,NO,NI]),[pri(cred,[I,KM,D,NO,NI])]).

% parelsnoer pseudocode
elneeded(pri(pc,[S,_,RD]),RD,[S]).
elneeded(pri(pc,[S,BSN,_]),BSN,[S]).


